(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #x6417453146339921) #xcdf45d675ce6336e))
(constraint (= (f #x02cb722951ca3e33) #x0000000000000001))
(constraint (= (f #x8ebbe7968a88616b) #xb8a20c34babbcf4b))
(constraint (= (f #xe8cdb39ec38bbe56) #x0000e8cdb39ec38c))
(constraint (= (f #x3051d46ea77ae2c6) #xe7d715c8ac428e9d))
(constraint (= (f #x0dd479648e93b87c) #x00000dd479648e94))
(constraint (= (f #x10c96835a656a09a) #x000010c96835a657))
(constraint (= (f #x135a1242c95e5a70) #x0000135a1242c95f))
(constraint (= (f #x5c4903d8a7845590) #x00005c4903d8a785))
(constraint (= (f #xb8dc00de43627d17) #x0000000000000001))
(constraint (= (f #x0e41023ca3c69cbe) #x00000e41023ca3c7))
(constraint (= (f #x4958d2d44a45aa0d) #xdb539695dadd2af8))
(constraint (= (f #xc61c113d3901eeb4) #x0000c61c113d3902))
(constraint (= (f #xcd95e1809c90c4e9) #x99350f3fb1b79d8a))
(constraint (= (f #x439b7b0a69b65e0e) #xde32427acb24d0f9))
(constraint (= (f #x4cb5d2533e96d9d5) #x0000000000000001))
(constraint (= (f #xcea4debee5b069ca) #x98ad90a08d27cb1b))
(constraint (= (f #xe5aa80663da0a3e1) #x8d2abfcce12fae0e))
(constraint (= (f #x86e3e9e64ebe269d) #x0000000000000001))
(constraint (= (f #x3293ab1d4daee6d7) #x0000000000000001))
(constraint (= (f #xaa14819e1ea3ce78) #x0000aa14819e1ea4))
(constraint (= (f #xce7d1e08b3936a11) #x0000000000000001))
(constraint (= (f #x2ee1a3cd34c7a42a) #xe88f2e19659c2deb))
(constraint (= (f #xeda51b88638c0386) #x892d723bce39fe3d))
(constraint (= (f #x4eb5ca0936ee2739) #x0000000000000001))
(constraint (= (f #x7a532208bd3ddb73) #x0000000000000001))
(constraint (= (f #xebc52b481982669c) #x0000ebc52b481983))
(constraint (= (f #xece58ee7d0e4a5e1) #x898d388c178dad0e))
(constraint (= (f #x9c40bea681d99b3d) #x0000000000000001))
(constraint (= (f #x3554ed0eba86c8c1) #xe5558978a2bc9b9e))
(constraint (= (f #xdc179a8689c37ba2) #x91f432bcbb1e422f))
(constraint (= (f #x3554ba9111295aed) #xe555a2b7776b5288))
(constraint (= (f #x6ec43ea284ccc633) #x0000000000000001))
(constraint (= (f #x3aece98c1ada5321) #xe2898b39f292d66e))
(constraint (= (f #xee63632d200ec914) #x0000ee63632d200f))
(constraint (= (f #x3b2ed902beecdc01) #xe268937ea08991fe))
(constraint (= (f #xee1c20708b0e3866) #x88f1efc7ba78e3cd))
(constraint (= (f #x991bd11d9a803a91) #x0000000000000001))
(constraint (= (f #x068c83734c43e0c0) #xfcb9be4659de0f9e))
(constraint (= (f #xd41ad08ccc5eb05c) #x0000d41ad08ccc5f))
(constraint (= (f #x7a7e27e1ee258dc3) #xc2c0ec0f08ed391f))
(constraint (= (f #x2ee34986e8531cdc) #x00002ee34986e854))
(constraint (= (f #xace464b77e499058) #x0000ace464b77e4a))
(constraint (= (f #x5e80de452249b3da) #x00005e80de45224a))
(constraint (= (f #x4e1cd283581aee4e) #xd8f196be53f288d9))
(constraint (= (f #xeceb7328d30382b1) #x0000000000000001))
(constraint (= (f #x7e89384e17500aa7) #xc0bb63d8f457faad))
(constraint (= (f #x139a88047623466b) #xf632bbfdc4ee5ccb))
(constraint (= (f #x053e9598ee274d48) #xfd60b53388ec595a))
(constraint (= (f #xc5ba7d6c16abe42e) #x9d22c149f4aa0de9))
(constraint (= (f #x9d5b3872826963e7) #xb15263c6becb4e0d))
(constraint (= (f #x6555559e57d468d3) #x0000000000000001))
(constraint (= (f #x21b8016673ce6de8) #xef23ff4cc618c90a))
(constraint (= (f #x8bb64d8edb21c941) #xba24d938926f1b5e))
(constraint (= (f #xdcbbee21381ded49) #x91a208ef63f1095a))
(constraint (= (f #x631adb6a6a9892bc) #x0000631adb6a6a99))
(constraint (= (f #xbd4dc908e030138e) #xa1591b7b8fe7f639))
(constraint (= (f #x77563a40c49309e3) #xc454e2df9db67b0f))
(constraint (= (f #x8a1dc249c84ee412) #x00008a1dc249c84f))
(constraint (= (f #x617bee27a6269ca5) #xcf4208ec2cecb1ac))
(constraint (= (f #x30694eaac156e347) #xe7cb58aa9f548e5d))
(constraint (= (f #xc3d2ddad2ee49a04) #x9e169129688db2fc))
(constraint (= (f #x73dcb932a4b2c666) #xc611a366ada69ccd))
(constraint (= (f #x634ee980b66a53a3) #xce588b3fa4cad62f))
(constraint (= (f #x6bc22b4e1eebd1be) #x00006bc22b4e1eec))
(constraint (= (f #x485568c46a3ecb15) #x0000000000000001))
(constraint (= (f #xe91ca9e4680a6718) #x0000e91ca9e4680b))
(constraint (= (f #x7b6292ae70e44d5e) #x00007b6292ae70e5))
(constraint (= (f #x5a8d8024e8c0be3a) #x00005a8d8024e8c1))
(constraint (= (f #x960cc93277713aea) #xb4f99b66c447628b))
(constraint (= (f #xee97ce9851eee339) #x0000000000000001))
(constraint (= (f #x54c7c6e82126e355) #x0000000000000001))
(constraint (= (f #x4b9250d2583081e7) #xda36d796d3e7bf0d))
(constraint (= (f #x1d0ec80e0ce4a481) #xf1789bf8f98dadbe))
(constraint (= (f #xd32a74dada312e30) #x0000d32a74dada32))
(constraint (= (f #xb3b4e5b7b956ee3d) #x0000000000000001))
(constraint (= (f #x0904193385bd57e8) #xfb7df3663d21540a))
(constraint (= (f #x50ea305e690a1c56) #x000050ea305e690b))
(constraint (= (f #xa6ed98dc599d589c) #x0000a6ed98dc599e))
(constraint (= (f #xb7b74ba3c9365215) #x0000000000000001))
(constraint (= (f #x63eeeabd8e204951) #x0000000000000001))
(constraint (= (f #xcec0a582dbe08862) #x989fad3e920fbbcf))
(constraint (= (f #xc05bd539e62deebc) #x0000c05bd539e62e))
(constraint (= (f #xda8e7debcc01a3a2) #x92b8c10a19ff2e2f))
(constraint (= (f #xa3e9e1c8d5a3d57a) #x0000a3e9e1c8d5a4))
(constraint (= (f #x1580c4e63a78a32b) #xf53f9d8ce2c3ae6b))
(constraint (= (f #xe7e6042aae8b6e6b) #x8c0cfdeaa8ba48cb))
(constraint (= (f #x4d5e017591e636dd) #x0000000000000001))
(constraint (= (f #xb49338ee5ecc507d) #x0000000000000001))
(constraint (= (f #xa035ec1ee85ee562) #xafe509f08bd08d4f))
(constraint (= (f #x49560e79165ca19e) #x000049560e79165d))
(constraint (= (f #x6878754466580249) #xcbc3c55dccd3feda))
(constraint (= (f #x300564ce942c47ee) #xe7fd4d98b5e9dc09))
(constraint (= (f #x27e71305676c98d4) #x000027e71305676d))
(constraint (= (f #x72cae5e6a2836bbd) #x0000000000000001))
(constraint (= (f #x5bbbbde553c47667) #xd222210d561dc4cd))
(constraint (= (f #x78aa8e6be2708e81) #xc3aab8ca0ec7b8be))
(constraint (= (f #x3a5c8e0d4ece425d) #x0000000000000001))
(constraint (= (f #x4135cce46696a731) #x0000000000000001))
(constraint (= (f #x2e78e2c05eab7ac9) #xe8c38e9fd0aa429a))
(check-synth)
